Nuprl Definition : ma-trivial-interface
11,40
postcript
pdf
ma-trivial-interface(
i
;
k
;
V
;
f
) ==
i
: <
,
k
: <
V
,
s
,
v
.
f
(
v
)>>
latex
Definitions
,
x
:
v
,
<
a
,
b
>
,
x
.
A
(
x
)
,
f
(
a
)
FDL editor aliases
ma-trivial-interface
origin
, k : <V, 
s,v. f(v)>> , k : <V, s,v. f(v)>> x.A(x)